Inference at * 2 
Iof proof for Lemma nth tl append:



1. T : Type
2. T List
3. u : T
4. v : T List
5. bs:(T List). nth_tl(||v||;v @ bs) ~ bs
  bs:(T List). nth_tl(||v||+1;[u / (v @ bs)]) ~ bs 

latex

 by ParallelLast 

latex

 1: 

 1: 5. bs : T List
 1: 6. nth_tl(||v||;v @ bs) ~ bs
 1:   nth_tl(||v||+1;[u / (v @ bs)]) ~ bs
 .

Definitions

t  T, n+m, #$n, [car / cdr], nth_tl(n;as), ||as||, as @ bs, x:A. B(x), x:AB(x), type List, s ~ t, Type